structure UTIL = struct
structure A = ABSTRACT
structure C = CONCRETE_REPRESENTATION
open ENV
open ABSTRACT_REPRESENTATION

(* ============================================================================================= *)
val crlf = "\n" (* line-separator (carriage-return, line-feed); windows: "\r\n", *nix/mac: "\n"  *)

(* ============================================================================================= *)
fun println msg = print(msg ^ crlf)

(* =============================================================================================
 * Converts NODE_INFO to a string representation of the form: lineLow.columnLow-lineHigh.columnHigh
 * ============================================================================================= *)
fun ninfoToString (C.info {line=(llo,lhi),column=(clo,chi)})
(*fun ninfoToString (C.info {line=(llo,lhi),column=(clo,chi), label=label_info})*)
      = Int.toString llo ^ "." ^ Int.toString clo ^ "-" ^ Int.toString lhi ^ "." ^ Int.toString chi ^ " "

(* =============================================================================================
 * Auxiliary functions to raise type errors with properly formatted error messages.
 * ============================================================================================= *)
fun raiseOpEqError(ty1, ty2, expr)
      = raise TypeError(ninfoToString (A.getExprInfo expr) ^
                        "Type error: types of operands don't agree:" 	^ crlf ^
                        "  left operand:  " ^ deepToString ty1 ^ crlf ^
                        "  right operand: " ^ deepToString ty2 ^ crlf ^
                        "  in expression: " ^ A.leavesToString expr false )

fun raiseTautologyError taut expr
      = raise TypeError(ninfoToString (A.getExprInfo expr) ^
                        "Type error: expression always succeeds/fails, " 	^
                        "attempting to create/negate a tautology" 				^ crlf ^
                        "  expression:    " ^ A.leavesToString taut false ^ crlf ^
                        "  in expression: " ^ A.leavesToString expr false )

fun raiseOperandError(actualTy, expectedTy, expr)
      = raise TypeError(ninfoToString (A.getExprInfo expr) ^
                        "Type error: operator and operand don't agree:" ^ crlf ^
                        "  expected: " ^ toString expectedTy            ^ crlf ^
                        "  found:    " ^ toString actualTy              ^ crlf ^
                        "  in expression:   " ^ A.leavesToString expr false )

fun raisePolyOpError(ty1, expr)
      = raise TypeError(ninfoToString (A.getExprInfo expr) ^
                        "Type error: overloaded operator not defined for this type:" ^ crlf ^
                        "  type:          " ^ toString ty1                           ^ crlf ^
                        "  in expression: " ^ A.leavesToString expr false )

fun raiseAppError s t expr msg
      = raise TypeError(ninfoToString (A.getExprInfo expr) ^
                        "Type error: " ^ msg ^ crlf ^
                        "  strategy: " ^ toString s ^ crlf ^
                        "  term:     " ^ toString t ^ crlf ^
                        "  in expression:  " ^ A.leavesToString expr false)

fun raiseCompositionError left right expr msg
      = raise TypeError(ninfoToString (A.getExprInfo expr) ^
                        "Type error: " ^ msg ^ crlf ^
                        "  left operand:  " ^ toString left ^ crlf ^
                        "  right operand: " ^ toString right ^ crlf ^
                        "  in expression: " ^ A.leavesToString expr false)

fun raiseTypeError expr msg
      = raise TypeError(ninfoToString (A.getExprInfo expr) ^
                        msg ^ crlf ^
                        "  in expression:  " ^ A.leavesToString expr false)

(* ============================================================================================= *)

(* ============================================================================================= *)
fun inferPrimType(a as TyTerm(s,[]))
    = if isSome(Bool.fromString s)
      then TyBool
      else if List.exists (fn c => c = #".") (String.explode s) andalso isSome(Real.fromString s)
           then TyReal
           else if isSome(Int.fromString s)
                then TyInt
                else if String.isPrefix "\"" s andalso String.substring(s,String.size(s)-1,1)="\""
                     then TyString
                     else a

fun pickATree (p as TyTerm _  , _               ) = p
  | pickATree ( _             , p as TyTerm _   ) = p
  | pickATree (ty1            , _               ) = ty1

fun skipNonBoolExpr (m as APP (ID   _,_,_) ) _ p = raiseTautologyError m p
  | skipNonBoolExpr (m as APP (SKIP _,_,_) ) _ p = raiseTautologyError m p
  | skipNonBoolExpr (     APP (_,     _,_) ) _ _ = TyBool
  | skipNonBoolExpr  _ actualTy                _ = actualTy

fun convertLeafsToPrims term1
    = mapTy (fn (a as TyTerm(x,[])) => inferPrimType a
                | x => x) term1

fun equalModPrims term1 term2 = convertLeafsToPrims term1 = convertLeafsToPrims term2

fun replaceLeaf tyChoices term1
    = let
          fun aux leafTy (x::xs) = if leafTy = x then x else aux leafTy xs
            | aux leafTy [] = raise TypeError("Impossible: replaceLeaf is invoked after unification.")
      in
          mapTy (fn (a as TyTerm(x,[])) => aux (inferPrimType a) tyChoices
                  | x => x) term1
      end
(* ============================================================================================= *)

fun listToString lst = foldr (op ^) "" lst

(* =============================================================================================
 * Auxiliary functions for folding abstract and concrete trees.
 * ============================================================================================= *)
(* foldNode: (INODE * 'a) -> 'a -> (INODE * 'a) -> 'a *)
fun foldNode f (p as inode _     , acc) = f(p, acc)
  | foldNode f (p as imatch_var _, acc) = f(p, acc)

(* foldTerm: (INODE * 'a) -> 'a -> (ITREE * 'a) -> 'a *)
fun foldTerm f (itree (root, children), acc) = foldr (foldTerm f) (f(root, acc)) children

(* foldExpr: (EXPR * 'a) -> 'a -> (ITREE * 'a) -> 'a -> (EXPR * 'a) -> 'a *)
fun foldExpr f g (p as PROG      (exprList,_) , acc) = f(p, foldl (foldExpr f g) acc exprList)
  | foldExpr f g (p as SIGNATURE     (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as LIST       (exprList,_), acc) = f(p, foldl (foldExpr f g) acc exprList)

  | foldExpr f g (p as RECURSIVE (expr1,exprList,expr2,_), acc)
      = f(p, foldExpr f g (expr2, (foldl (foldExpr f g) (foldExpr f g (expr1,acc)) exprList) ) )

  | foldExpr f g (p as NON_RECURSIVE (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )

  | foldExpr f g (p as ITERATOR(expr1,exprs,_), acc) = f(p, foldl (foldExpr f g) (foldExpr f g (expr1,acc)) exprs)
  | foldExpr f g (p as MAPL          (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as MAPR          (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as MAPB          (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )

  | foldExpr f g (p as FOLD_CHOICE   (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLD_LCHOICE  (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLD_RCHOICE  (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLD_LSEQ     (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLD_RSEQ     (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLD_LSTAR    (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLD_RSTAR    (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLDS_CHOICE  (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLDS_LCHOICE (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLDS_RCHOICE (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLDS_LSEQ    (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLDS_RSEQ    (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLDS_LSTAR   (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as FOLDS_RSTAR   (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )

  | foldExpr f g (p as CHOICE  (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as LCHOICE (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as RCHOICE (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as LSEQ    (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as RSEQ    (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as LSTAR   (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as RSTAR   (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )

  | foldExpr f g (p as TRANSIENT     (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as OPAQUE        (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as RAISE         (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as HIDE          (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as LIFT          (expr1,_), acc) = f(p, foldExpr f g (expr1,acc) )

  | foldExpr f g (p as APP     (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )

  | foldExpr f g (p as RULE     (expr1,expr2     ,_),acc)= f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as COND_RULE(expr1,expr2,cond,_),acc)= f(p, foldExpr f g (expr2, foldExpr f g (cond, foldExpr f g (expr1,acc))))

  | foldExpr f g (p as MATCH   (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as BIND    (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as ANDALSO (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as ORELSE  (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as NOT     (expr1      ,_), acc) = f(p, foldExpr f g (expr1,acc) )

  | foldExpr f g (p as LIBRARY_CALL_0 (expr1,_)         , acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as LIBRARY_CALL   (expr1,exprList,_), acc) = f(p, foldl (foldExpr f g) (foldExpr f g (expr1,acc)) exprList)

  | foldExpr f g (p as B_OR    (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as B_AND   (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as BANG    (expr1      ,_), acc) = f(p, foldExpr f g (expr1,acc) )
  | foldExpr f g (p as EQ      (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as NEQ     (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as LEQ     (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as LT      (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as GEQ     (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as GT      (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as CONCAT  (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as PLUS    (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as MINUS   (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as TIMES   (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as DIVIDE  (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as DIV     (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as MOD     (expr1,expr2,_), acc) = f(p, foldExpr f g (expr2, foldExpr f g (expr1,acc) ) )
  | foldExpr f g (p as TILDE   (expr1      ,_), acc) = f(p, foldExpr f g (expr1,acc) )

  | foldExpr f g (     TERM             (t1,_), acc) = g(t1,acc)
  | foldExpr f g (p as REF                  _ , acc) = f(p, acc)
  | foldExpr f g (p as BOOL                 _ , acc) = f(p, acc)
  | foldExpr f g (p as INT                  _ , acc) = f(p, acc)
  | foldExpr f g (p as REAL                 _ , acc) = f(p, acc)
  | foldExpr f g (p as STRING               _ , acc) = f(p, acc)
  | foldExpr f g (p as IDENTIFIER           _ , acc) = f(p, acc)
  | foldExpr f g (p as ID                   _ , acc) = f(p, acc)
  | foldExpr f g (p as SKIP                 _ , acc) = f(p, acc)
  | foldExpr f g (p as TRUE                   , acc) = f(p, acc)
  | foldExpr f g (p as FALSE                  , acc) = f(p, acc)
(* ============================================================================================= *)

(* For use in folding lists. *)
fun myOr (x,acc) = acc orelse x
fun myAnd(x,acc) = acc andalso x

(* flattenSums: ty list list -> ty list -> ty list list *)
fun flattenSums acc (TySum(x,y)::xs)
      = let
            val choice1 = map (fn aList => x::aList) acc
            val choice2 = map (fn aList => y::aList) acc
            val deepChoice1 = foldr (op @) [] (map (flattenSums [[]]) choice1)
            val deepChoice2 = foldr (op @) [] (map (flattenSums [[]]) choice2)
        in
            flattenSums (deepChoice1@deepChoice2) xs
        end
  | flattenSums acc (x::xs) = flattenSums (map (fn aList => x::aList) acc) xs
  | flattenSums acc []      = map (List.rev) acc


(* =============================================================================================
 * Remembers the program tree for proper re-orientation of match equations during type analysis. *)
val inputTree = ref (TERM (itree (inode "", []), info {line=(0,0), column=(0,0)}) )
(*val inputTree = ref (TERM (itree (inode("", C.default_info), []), info {line=(0,0), column=(0,0), label=""}) )*)

(* Boolean constant defining the mode of the type-checker: in or out of regression testing.*)
val inTestingMode = ref false

(* Type-checking can be performed at varying levels of precision: 
     0: rewrite rules only
     1: level 0 and combinators
     2: level 1 and fold operators
     3: level 2 and one-layer iterators
     4: level 3 and full iterators
   By default, analysis is performed at level 0. *)
val precision = ref 0;

(* Verbosity level: 
     0: OFF:    no logging
     1: ERROR:  log only error messages
     2: WARNING:level 1 and warnings
     3: INFO:   level 2 and info messages
     4: DEBUG:  level 3 and debug messages
     5: FINE:   level 4 and fine messages
     6: ALL:    log all messages
   By default, verbosity is at level 3. *)
val verbosity = ref 3
val indent = ref ""
fun push() = indent := !indent ^ " "
fun pop()  = indent := implode(tl(explode (!indent)))
fun decode flag msg = case flag of
                        0 => println(!indent ^ msg)
                      | 1 => (push(); println(!indent ^ msg))
                      | 2 => (push(); println(!indent ^ msg); pop())
                      | _ => (println(!indent ^ msg); pop())
fun error   msg flag = if !verbosity < 1 then () else decode flag msg
fun warning msg flag = if !verbosity < 2 then () else decode flag msg
fun info    msg flag = if !verbosity < 3 then () else decode flag msg
fun debug   msg flag = if !verbosity < 4 then () else decode flag msg
fun fine    msg flag = if !verbosity < 5 then () else decode flag msg

type configuration = {precision: int, verbosity: int}

fun init prec verb
    = (inTestingMode := false; (* set to false to skip assertion-checking/regression-testing *)
	     precision := prec;      (* precision levels of type-checking from 0 to 4 in the increasing order *)
	     verbosity := verb       (* verbosity of output from 0 to 6 in the increasing order *)
      )
end